P:(), d:(n:. Dec(P(n))). (n:. P(n))  {P(mu(d)) & (i:. (i < mu(d))  (P(i)))} 

latex

Definitions	x:AB(x), , Dec(P), x:A. B(x), {i..j}, #$n, {T}, P & Q, x:A. B(x), , P  Q, a < b, mu(f), A, x(s), n - m, n+m, -n, A  B, False, Void, i  j , t  T, {x:A| B(x)} , Type, f(a), x:A  B(x), if b then t else f fi , , x.A(x), , b, s = t, i  j < k, P  Q, left + right, s ~ t, SQType(T), True, T
Lemmas	not wf, mu-wf2, decidable int equal, decidable wf, le wf, nat wf, mu wf, ifthenelse wf, nat properties, ge wf